(*
 * Copyright (c) 2001-2009,
 *  George C. Necula    <necula@cs.berkeley.edu>
 *  Scott McPeak        <smcpeak@cs.berkeley.edu>
 *  Wes Weimer          <weimer@cs.berkeley.edu>
 *  Collin Engstrom     <technobug@gmail.com>
 *  Jacob Burnim        <jburnim@cs.berkeley.edu>
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 * 1. Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 *
 * 2. Redistributions in binary form must reproduce the above copyright
 * notice, this list of conditions and the following disclaimer in the
 * documentation and/or other materials provided with the distribution.
 *
 * 3. The names of the contributors may not be used to endorse or promote
 * products derived from this software without specific prior written
 * permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
 * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
 * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
 * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
 * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
 * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
 * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
 * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
 * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 *)

open Pretty
open Cil
open Printf
module E = Errormsg
module H = Hashtbl

(* Read list of changes from file. *)
let filename = "changefile.dat";;
let load_file filename =
  let ic = open_in filename in
  let rec lf ichan acc =
    try
      lf ic (int_of_string(input_line ic)::acc)
    with End_of_file -> (acc : int list)
  in
let res = lf ic[] in
  close_in ic; res;;

let varCounter = ref 0 ;;

let do_changes = load_file filename;;

let writeCount filename (cnt:int) =
  try
    let oc = open_out filename in
    Printf.fprintf oc "%d" cnt;
    close_out oc
  with x ->
    failwith("Failed to write counter to: "^filename^"\n")


(* David Park at Stanford points out that you cannot take the address of a
 * bitfield in GCC. *)

(* Returns true if the given lvalue offset ends in a bitfield access. *)
let rec is_bitfield lo = match lo with
  | NoOffset -> false
  | Field(fi,NoOffset) -> not (fi.fbitfield = None)
  | Field(_,lo) -> is_bitfield lo
  | Index(_,lo) -> is_bitfield lo

(* Return an expression that evaluates to the address of the given lvalue.
 * For most lvalues, this is merely AddrOf(lv). However, for bitfields
 * we do some offset gymnastics.
 *)
let addr_of_lv (lh,lo) =
  if is_bitfield lo then begin
    (* we figure out what the address would be without the final bitfield
     * access, and then we add in the offset of the bitfield from the
     * beginning of its enclosing comp *)
    let rec split_offset_and_bitfield lo = match lo with
      | NoOffset -> failwith "logwrites: impossible"
      | Field(fi,NoOffset) -> (NoOffset,fi)
      | Field(e,lo) ->  let a,b = split_offset_and_bitfield lo in
                        ((Field(e,a)),b)
      | Index(e,lo) ->  let a,b = split_offset_and_bitfield lo in
                        ((Index(e,a)),b)
    in
    let new_lv_offset, bf = split_offset_and_bitfield lo in
    let new_lv = (lh, new_lv_offset) in
    let enclosing_type = TComp(bf.fcomp, []) in
    let bits_offset, bits_width =
      bitsOffset enclosing_type (Field(bf,NoOffset)) in
    let bytes_offset = bits_offset / 8 in
    let lvPtr = mkCast ~e:(mkAddrOf (new_lv)) ~newt:(charPtrType) in
    (BinOp(PlusPI, lvPtr, (integer bytes_offset), ulongType))
  end else (AddrOf (lh,lo))


class floatddInstrumentVisitor (f: file) =
 (* let counter : varinfo = ref None in*)

  let makeCounter () : varinfo =
      let m = makeGlobalVar "__floatCounter__" (TInt(IInt, [])) in
        f.globals <- GVarDecl (m, locUnknown) :: f.globals;(* counter building code *)

      m
  in

  let makeExpCounter () : varinfo =
      let m = makeGlobalVar "__floatExpCounter__" (TInt(IInt, [])) in
        f.globals <- GVarDecl (m, locUnknown) :: f.globals;(* counter building code *)

      m
  in



  let isFloat f : bool =
    match f with
      | TFloat (FFloat , _) -> true
      | _                  -> false
  in

  let isPromote (c:int)  =
    List.mem c do_changes;
  in

  let doPromote (v:varinfo)  =

    v.vtype <- Cil.doubleType;

  in



  let counter = makeCounter() in
  let expCounter = makeExpCounter() in



object (self)
  inherit nopCilVisitor
  val printfFun =
    let fdec = emptyFunction "printf" in
    fdec.svar.vtype <- TFun(intType,
                            Some [ ("format", charConstPtrType, []) ],
                            true, []);
    fdec

(********************************************************************************************************)

  method vvdec (v: varinfo) : varinfo visitAction =

    if (isFloat v.vtype = true) then begin
      varCounter := !varCounter + 1;


    if (isPromote  (!varCounter)  ) = true then begin (*Check counter and promote if it's in list*)
         doPromote v;
         DoChildren

     end

     else DoChildren;
   end
else DoChildren;





(********************************************************************************************************)

  method vexpr (e: exp) : exp visitAction=
    (*let tmp = List.hd[] in*)

    match e with
        | Const c                  -> DoChildren
        | Lval lb                  -> DoChildren
        | CastE (t, e1)            -> begin if not ((*t = Cil.doubleType*) isFloat t = true) then SkipChildren
                                      else let str = Pretty.sprint 80
                                                (Pretty.dprintf "Float cast has occurred. %%i\n") in
                                                self#queueInstr ([

                                                                   Set (((Var(expCounter)), NoOffset),
                                                                        BinOp(PlusA, Lval((Var(expCounter)), NoOffset), one, Cil.intType),
                                                                        locUnknown) ;

                                                                   Call((None),
                                                                        (Lval(Var(printfFun.svar),NoOffset)),
                                                                        [ mkString str; Lval((Var(expCounter)), NoOffset)],
                                                                        locUnknown)

                                                                   (*doPromote(expCounter);*)

                                                                ]);
                                      DoChildren
                                      end

        | UnOp (op, e1, t)         -> begin if not ((*t = Cil.doubleType*) isFloat t = true) then SkipChildren
                                      else let str = Pretty.sprint 80
                                                (Pretty.dprintf "Float unary has occurred. %%i\n") in
                                                self#queueInstr ([

                                                                   Set (((Var(expCounter)), NoOffset),
                                                                        BinOp(PlusA, Lval((Var(expCounter)), NoOffset), one, Cil.intType),
                                                                        locUnknown) ;

                                                                   Call((None),
                                                                        (Lval(Var(printfFun.svar),NoOffset)),
                                                                        [ mkString str; Lval((Var(expCounter)), NoOffset)],
                                                                        locUnknown)

                                                                ]);
                                      DoChildren
                                      end

         | BinOp (op, e1, e2, t)    -> begin if not ((*t = Cil.doubleType*) isFloat t = true) then SkipChildren
                                       else let str = Pretty.sprint 80
                                                (Pretty.dprintf "Float binary has occurred. %%i\n") in
                                                self#queueInstr ([

                                                                   Set (((Var(expCounter)), NoOffset),
                                                                        BinOp(PlusA, Lval((Var(expCounter)), NoOffset), one, Cil.intType),
                                                                        locUnknown) ;

                                                                   Call((None),
                                                                        (Lval(Var(printfFun.svar),NoOffset)),
                                                                        [ mkString str; Lval((Var(expCounter)), NoOffset)],
                                                                        locUnknown)

                                                                ]);
                                      DoChildren
                                      end

         | _                        -> DoChildren

(********************************************************************************************************)


  method vinst (i: instr) : instr list visitAction =
    match i with
      Set(lv, e, l) -> begin
        (* Check if we need to log *)

        match lv with
          (Var(v), off) when not (isFloat v.vtype = true) -> SkipChildren
        | _ ->	let str = Pretty.sprint 80
                (Pretty.dprintf "Float assignment has occurred. %%i\n" )

              in

              self#queueInstr
              ([

                  Set (((Var(counter)), NoOffset),
                       BinOp(PlusA, Lval((Var(counter)), NoOffset), one, Cil.intType),
                       locUnknown) ;

                  Call((None),
                       (Lval(Var(printfFun.svar),NoOffset)),
                       [ mkString str; Lval((Var(counter)), NoOffset)],
                       locUnknown)



              ]);
              DoChildren


      end
    | Call(Some lv, f, args, l) -> begin
        (* Check if we need to log *)
        match lv with
          (Var(v), off) when not (isFloat v.vtype = true) -> SkipChildren
        | _ -> let str = Pretty.sprint 80
                (Pretty.dprintf "Float assignment has occurred.\n" )

              in
              self#queueInstr
              ([

                  Set (((Var(counter)), NoOffset),
                       BinOp(PlusA, Lval((Var(counter)), NoOffset), one, Cil.intType),
                       locUnknown) ;

                  Call((None),
                       (Lval(Var(printfFun.svar),NoOffset)),
                       [ mkString str; Lval((Var(counter)), NoOffset)],
                       locUnknown)

              ]);
              DoChildren
      end
    | _ -> SkipChildren

end

(********************************************************************************************************)

let feature : featureDescr =
  { fd_name = "floatddInstrument";
    fd_enabled = ref false;
    fd_description = "instrument code for floating-point delta debugging";
    fd_extraopt = [];
    fd_doit =
    (function (f: file) ->
      let fddiVisitor = new floatddInstrumentVisitor f in
      visitCilFileSameGlobals fddiVisitor f;
      writeCount "floatCount.dat" !varCounter);
    fd_post_check = true;
  }
